/*
 * Copyright 2012 Fabian Wenzelmann
 * 
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 * 
 * Recognition-Procedures-for-Boolean-Functions is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.  If not, see <http://www.gnu.org/licenses/>.
 */

package de.wenzelmf.booleanFunction.booleanExpression;

import java.util.Iterator;
import java.util.LinkedList;
import java.util.Queue;

import de.wenzelmf.booleanFunction.util.IStack;
import de.wenzelmf.booleanFunction.util.LinkedListStack;
import de.wenzelmf.booleanFunction.util.Tuple;

/**
 * This class can be used to evaluate the truth value of a given Boolean expression.
 * 
 * The method {@link BooleanExpression#getTruthValue(Assignment)} is usually defined in
 * a recursive way and Java will give up very fast. This class defines a iterative
 * evaluation function.
 * 
 * @author Fabian Wenzelmann
 * @version 1.0
 *
 */
public class Evaluator
{
	/**
	 * An public Evaluator object with recursive threshold 3.
	 */
	public static final Evaluator EVALUATOR = new Evaluator(3);
	
	/*
	 * The threshold when we use the iterative method instead of the recursive one.
	 */
	private int recursiveThreshold;
	
	/**
	 * Constructor method.
	 * 
	 * @param recursiveThreshold You can specify if for "small" formulae the recursive method
	 * should be applied, so for all formulae with complete size less or equal than
	 * <code>recursiveThreshold</code> the recursive method {@link BooleanExpression#getTruthValue(Assignment)}
	 * will be used.
	 */
	public Evaluator(int recursiveThreshold)
	{
		this.recursiveThreshold = recursiveThreshold;
	}
	
	/**
	 * Creates a new Evaluator that always uses the iterative method.
	 */
	public Evaluator()
	{
		this(-1);
	}
	
	/**
	 * Returns the truth value of &phi; given the assignment &alpha;.
	 * @param phi The Boolean expression.
	 * @param alpha The assignment.
	 * 
	 * @return <code>true</code> if &alpha; &#8872; &phi;.
	 */
	public boolean getTruthValue(BooleanExpression phi, Assignment alpha)
	{
		if(phi.completeSize() <= recursiveThreshold)
		{
			return phi.getTruthValue(alpha);
		}
		IStack<Tuple<BooleanExpression, Integer>> evalStack = new LinkedListStack<Tuple<BooleanExpression, Integer>>();
		final boolean[] results = new boolean[phi.completeSize()];
		
		Queue<Tuple<BooleanExpression, Integer>> working = new LinkedList<Tuple<BooleanExpression, Integer>>();
		
		Tuple<BooleanExpression, Integer> root = new Tuple<BooleanExpression, Integer>(phi, 0);
		evalStack.push(root);
		working.add(root);
		
		while(!working.isEmpty())
		{
			Tuple<BooleanExpression, Integer> next = working.poll();
			// first child is one position after this
			int nextPos = next.getSecond() + 1;
			for(BooleanExpression sub : next.getFirst())
			{
				// add this child to the next position
				Tuple<BooleanExpression, Integer> nextEntry = new Tuple<BooleanExpression, Integer>(sub, nextPos);
				working.add(nextEntry);
				// TODO: test!
				evalStack.push(nextEntry);
				nextPos += sub.completeSize();
			}
		}
		
		// now use the evaluation stack to calculate all recursive solutions
		while(!evalStack.isEmpty())
		{
			final Tuple<BooleanExpression, Integer> next = evalStack.pop();
			// evaluate the truth value of next!
			final BooleanExpression e = next.getFirst();
			if(e.getArity() <= 1)
			{
				// we have true, false or an atom, so simply calculate the truth value
				// given the assignment and put it to the right position
				results[next.getSecond()] = e.getTruthValue(alpha);
			}
			else
			{
				// we need the recursive solutions in the array
				Iterator<Boolean> recSolIterator = new Iterator<Boolean>()
						{
					
							Iterator<BooleanExpression> subFormIt = e.iterator();
							int pos = next.getSecond() + 1;
							
							@Override
							public boolean hasNext()
							{
								return subFormIt.hasNext();
							}

							@Override
							public Boolean next()
							{
								boolean result = results[pos];
								pos += subFormIt.next().completeSize();
								return result;
							}

							@Override
							public void remove()
							{
								throw new UnsupportedOperationException(
										"Removing elements from this Iterator is not allowed (Evaluator class).");
							}
					
						};
						results[next.getSecond()] = e.getFunction().getValue(recSolIterator);
			}
		}
		
		// result can be found on position 0
		return results[0];
	}
}